Nuprl Lemma : length-append
0,22
postcript
pdf
as
,
bs
:Top List. ||
as
@
bs
|| ~ (||
as
||+||
bs
||)
latex
Definitions
||
as
||
,
x
:
A
.
B
(
x
)
,
Top
,
t
T
Lemmas
top
wf
,
length
wf1
origin
as, bs:Top List. ||as @ bs|| ~ (||as||+||bs||) as, bs:Top List. ||as @ bs|| ~ (||as||+||bs||) x:A. B(x)
T